(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
plus(s(s(x)), y) → s(plus(x, s(y)))
plus(x, s(s(y))) → s(plus(s(x), y))
plus(s(0), y) → s(y)
plus(0, y) → y
ack(0, y) → s(y)
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, plus(y, ack(s(x), y)))
Rewrite Strategy: FULL
(1) CpxTrsToCpxRelTrsProof (BOTH BOUNDS(ID, ID) transformation)
Transformed TRS to relative TRS where S is empty.
(2) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
plus(s(s(x)), y) → s(plus(x, s(y)))
plus(x, s(s(y))) → s(plus(s(x), y))
plus(s(0), y) → s(y)
plus(0, y) → y
ack(0, y) → s(y)
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, plus(y, ack(s(x), y)))
S is empty.
Rewrite Strategy: FULL
(3) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(2n):
The rewrite sequence
ack(s(s(x52929_1)), s(s(s(x52701_1)))) →+ ack(x52929_1, plus(plus(x52701_1, s(ack(s(s(x52929_1)), s(s(x52701_1))))), ack(s(x52929_1), plus(x52701_1, s(ack(s(s(x52929_1)), s(s(x52701_1))))))))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1,0,1,0].
The pumping substitution is [x52701_1 / s(x52701_1)].
The result substitution is [ ].
The rewrite sequence
ack(s(s(x52929_1)), s(s(s(x52701_1)))) →+ ack(x52929_1, plus(plus(x52701_1, s(ack(s(s(x52929_1)), s(s(x52701_1))))), ack(s(x52929_1), plus(x52701_1, s(ack(s(s(x52929_1)), s(s(x52701_1))))))))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1,1,1,1,0].
The pumping substitution is [x52701_1 / s(x52701_1)].
The result substitution is [ ].
(4) BOUNDS(2^n, INF)